$\forall$$E$, $T$:Type. tree\_con($E$;$T$) $\in$ Type